Nuprl Lemma : normal-type_wf
0,22
postcript
pdf
T
:Type{i}. normal-type{i:l}(
T
)
Prop{i'}
latex
Definitions
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
AtomFree(
T
;
x
)
,
Prop
,
x
:
A
B
(
x
)
,
P
&
Q
,
Normal(
T
)
Lemmas
atom-free
wf
origin
T:Type{i}. normal-type{i:l}(T) 
Prop{i'} T:Type{i}. normal-type{i:l}(T) Prop{i'} Tx:A. B(x)
B(x)